@manuscript{Abadi:93,
title={{Types for the Scott Numerals}},
author={M. Abadi and L. Cardelli and G. Plotkin},
note="Unpublished, available from Abadi's web page",
year=1993,
pages={1--2}}                  

@misc{Pfu:2013,
title={Church Encoding with Dependent Types},
author={Fu, Peng and Stump, Aaron},
year=2013,
howpublished="Submitted, available from \url{http://homepage.cs.uiowa.edu/~pfu/document/papers/esop-2013.pdf}",

}                  

@book{Church:1985,
 author = {Church, Alonzo},
 title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
 year = {1985},
 isbn = {0691083940},
 publisher = {Princeton University Press},
 address = {Princeton, NJ, USA},
} 
@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  publisher = {North-Holland},
  year = {1972},
  pages = {xiv+520}
}

@article{Barendregt:97,
  author    = {Henk Barendregt},
  title     = {The impact of the lambda calculus in logic and computer
               science},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {3},
  number    = {2},
  year      = {1997},
  pages     = {181-215},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0302/0302-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@dissertation{Girard:72,
author="Jean-Yves Girard",
title="Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur",
institution="Universit\'e Paris VII",
year="1972"}

@book{Girard:1989,
 author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
 title = {Proofs and types},
 year = {1989},
 isbn = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 

@inproceedings{Werner:92,
author = {B. Werner},
title = {{A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}},
booktitle="International Workshop on Types for Proofs and Programs (TYPES)",
year="1992",
editor={B. Nordstr\"om and K. Petersson and G. Plotkin},
pages="341--357",
}
@article{Coquand:1988,
 author = {Coquand, Thierry and Huet, Gerard},
 title = {The calculus of constructions},
 journal = {Inf. Comput.},
 issue_date = {February/March 1988},
 volume = {76},
 number = {2-3},
 month = feb,
 year = {1988},
 issn = {0890-5401},
 pages = {95--120},
 numpages = {26},
 url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},
 doi = {10.1016/0890-5401(88)90005-3},
 acmid = {47725},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
} 
@incollection{Paulin:1993,
  title={Inductive definitions in the system coq rules and properties},
  author={Paulin-Mohring, Christine},
  booktitle={Typed lambda calculi and applications},
  pages={328--345},
  year={1993},
  publisher={Springer}
}
@article{Jansen:2011,
  author    = {J.M. Jansen and R. Plasmeijer and P. Koopman},
  title     = {Functional Pearl: Comprehensive Encoding of Data Types and Algorithms in the lambda-Calculus},
  journal   = {Internal report, NLDA},
  year      = {2011},
}
@article{Ariola:1997,
title = "Lambda Calculus with Explicit Recursion ",
journal = "Information and Computation ",
volume = "139",
number = "2",
pages = "154 - 233",
year = "1997",
note = "",
issn = "0890-5401",
doi = "10.1006/inco.1997.2651",
url = "http://www.sciencedirect.com/science/article/pii/S0890540197926511",
author = "Zena M. Ariola and Jan Willem Klop"
}
@article{CurienHL96,
  author    = {Pierre-Louis Curien and
               Th{\'e}r{\`e}se Hardin and
               Jean-Jacques L{\'e}vy},
  title     = {Confluence Properties of Weak and Strong Calculi of Explicit
               Substitutions},
  journal   = {J. ACM},
  volume    = {43},
  number    = {2},
  year      = {1996},
  pages     = {362-397},
  ee        = {http://doi.acm.org/10.1145/226643.226675},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Barendregt85,
    author = {Barendregt, H. P.},
    edition = {Revised},
    howpublished = {Paperback},
    isbn = {0444875085},
    keywords = {lambda},
    month = nov,
    posted-at = {2006-08-20 10:51:05},
    priority = {0},
    publisher = {North Holland},
    title = {{The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Revised Edition}},
    year = {1985}
}

@article{Hardin:1989,
 author = {Hardin, Th{\'e}r\`{e}se},
 title = {Confluence results for the pure strong categorical logic CCL. $\lambda$-calculi as subsystems of CCL},
 journal = {Theor. Comput. Sci.},
 issue_date = {July 1989},
 volume = {65},
 number = {3},
 month = jul,
 year = {1989},
 issn = {0304-3975},
 pages = {291--342},
 numpages = {52},
 url = {http://dx.doi.org/10.1016/0304-3975(89)90105-9},
 doi = {10.1016/0304-3975(89)90105-9},
 acmid = {70103},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
} 
@inproceedings{kuan2007,
  title={A rewriting semantics for type inference},
  author={Kuan, George and MacQueen, David and Findler, Robert Bruce},
  booktitle={Proceedings of the 16th European conference on Programming},
  pages={426--440},
  year={2007},
  organization={Springer-Verlag}
}

@phdthesis{hindley1964,
  title={The Church-Rosser property and a result in combinatory logic.},
  author={Hindley, James Roger},
  year={1964},
  school={University of Newcastle upon Tyne}
}
@article{Rosen:1973,
 author = {Rosen, Barry K.},
 title = {Tree-Manipulating Systems and Church-Rosser Theorems},
 journal = {J. ACM},
 issue_date = {Jan. 1973},
 volume = {20},
 number = {1},
 month = jan,
 year = {1973},
 issn = {0004-5411},
 pages = {160--187},
 numpages = {28},
 url = {http://doi.acm.org/10.1145/321738.321750},
 doi = {10.1145/321738.321750},
 acmid = {321750},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@inproceedings{stump2011,
  title={Type Preservation as a Confluence Problem.},
  author={Stump, Aaron and Kimmell, Garrin and Omar, Roba El Haj},
  booktitle={RTA},
  pages={345--360},
  year={2011}
}
